wpfacts, codegen: arrays held in class fields read under Rep::Arr, and field read calls inside the floor (P4 lever 1, PR-C3) - #14402

DESIGN-p4l1 rev 2 §3 (the field's rep, FactsField.rep, FieldProof.array as the join over the class set), §4.2 (the one tier, here for field reads and for b1, this.at(sq) = this.board[sq] ?? 0 behind a method), §2.8 (b1 stays export-time), §5.1-5.6 and §8's PR-C3 row, with REVIEW-p4l1's conditions for C3: finding 8 (hard.is_none(), join not meet, both already in PR-B's FieldFacts::rep), finding 13 (the sites that are not in the floor) and "the passed-pawn interval from the dump first".

Branch head: 3e926635b5. The branch merges current origin/main (482d9c9, with C2 #14394, P3 B3 #14395 and N6 #14396), by merge, not rebase; it merges cleanly with ba9234e.

What changes

• The field's rep reaches codegen (FactsField.rep, from wpfacts FieldFacts::rep, which PR-B computed with no consumer). A field has Arr when it is definite, a data field, its template is neither escaped nor hard, and every value its field node holds, over every token of the template, is a plain program Array.

• FieldProof.array is the join of that rep over the receiver's class set, None when some class's field is not Arr, and for a guarded or possibly absent read. wpfacts_access::field_array is the same join for a read however it is lowered (the field's value does not depend on the slot proof): an unchecked proven receiver, no interpreted code.

• One query for a receiver's rep (proven_array::receiver_rep): a local, parameter or module constant (BindingFacts::rep, C2), or a field read (FieldProof.array). A direct this.f[i] read then takes C2's tier unchanged: the key's interval at the site (element_keys) against the floor, the number test by number_element_reads.

• b1 inside the floor (§2.8). The method body's read joins every caller's key, so its own facts keep the bound, the hole test and the ??. wpfacts' FieldReadCall gains:

  • array: arr_rep over every copy (inlined, and one per summarized instance) of the body's element-read receiver, which is what the read reads from;
  • in_floor: array.dense, and this call's own key interval (call_arg_ranges) inside [0, array.floor).

  It is computed at export from the template's hole_free bit (PR-B's fused fill), the length floor and the call's key. It does not go through C1's ElemUndef, so it holds for an array that is stored into.

• The in-floor call in codegen (lower_call/field_read_call.rs). When the call is in the floor and the field read is Arr, dense, with a floor, the call is: the index as an int32, the field load, and the tier's in-floor read (proven_array::lower_in_floor): one and, the forwarding test when the storage can grow, the load at h + 24 + 8*i. With Number elements (rep.elem is F64 or I32) the value is never nullish and ?? L is the value. With Boxed elements and a ?? L the call keeps the read it had (a stored null or undefined is a present element).

• Not in the floor (make's at(captureSquare), set's at(square)): the rebuilt read this.f[k] ?? L goes through the tier as any field read does: forwarding test, idx <u capacity, load, hole compare, ??, cold arm.

The per-site verdicts (the dump; chess.ts)

PERRY_FACTS_DUMP prints one line per field read call: # field_read_call module= call= field= key=[lo,hi] rep= in_floor=. Chess has 35 such calls, all on Chess.board = arr<f64,128,dense> (growable: the store keys reach 255, so the forwarding test stays). 27 are in the floor, 8 are not:

The passed-pawn interval is settled: [0,255], not in the floor, so evaluate is at the low end of the design's range, and below it, because two more site classes the design counted in the floor are not. Both are the range analysis, not this PR:

• r*16 + f with r, f in [0,7]: the sum of two operands that both grow during the solve is widened past its hull. A probe with one method per shape (same binary, same dump) gives: at(r*16) [0,112] (exact); at(r + f) [0,127] (hull [0,14]); at(r*16 + f) [0,255] (hull [0,119]) when both loops count up, and [0,119] (exact) when r counts down from 7. The rungs are model::range::widen's ladder (7, 127, 255). Which growth takes the sum past 127 is not investigated.
• for (let square = 0; square < 128; square++) { if ((square & 0x88) !== 0) { square += 7; continue; } … this.at(square): gen/narrow.rs ends the narrowed reads at the body's first write of the counter in program text, also when that write is in a branch that always leaves (continue), so the read after the if sees the counter's whole interval, [0,255]. The same probe: with square += 7; continue; the key is [0,255], with a bare continue; it is [0,127].

Those reads take the outside-the-floor form (saving about half of the in-floor form). Follow-up, with its own census: see below.

Check mode, switch, sabotage

• PERRY_VERIFY_FACTS=1.
  • A field read whose proof has array: Some(r) tests the word it loaded (array_rep::witness_value, Fact::ArrayRep): heap band, GC_TYPE_ARRAY, not forwarded when fixed, length >= floor and capacity >= floor.
  • An in-floor call is tested where it loads (array_rep::witness_read): the claims above, no element descriptor, front offset 0, the key is below the call's floor, the slot is no hole and holds an element of rep.elem. b1's own witness stays: the real call runs beside the read and the two values must be the same bits.
• PERRY_FACTS_ARRAY_FIELDS=0: FieldFacts::rep is Boxed and no call is in the floor, which is C2's build (before the merge of main, the off arm's chess counts are C2's on arm to 0.1 M). It is a compile-cache input (compile_env.rs), and array_fact_switches_are_cache_inputs lists it.
• Sabotage arms, each with an S0 fixture that exits 0 when correct and 86 ("array rep") when sabotaged:
  • arrfield: a field's rep ignores the null/undefined its node also holds (array-field-negative.ts: the witness at the field read reports the null word);
  • arrb1: every call into a dense floor is in the floor, whatever its key (array-b1-negative.ts: keys ep - 16 and ep + 16 on a 16-element board; the tier's witness reports the key).

Results (qb9, instructions:u)

Build 9b04629446 (the head's code: the three later commits change two unit-test files and a comment in a parity fixture). On vs PERRY_FACTS_ARRAY_FIELDS=0 on the same binary, two runs each, checksums equal in every run.

Runs: search 30 754.3 / 30 754.4 on, 33 147.9 twice off; the other three identical between runs. Before the merge of main (build 8766d29dbe, without P3 B3 and N6): search 31 998.9 / 34 341.2 (−6.82%), perft 747.0 / 807.6 (−7.50%), evaluate 2 870.1 / 3 117.5 (−7.94%), legal 1 110.7–1 111.1 / 1 167.5 (−4.87%); that off arm equals C2's on arm to 0.1 M.

Search, perft and legal are at 79%, 86% and 87% of the design's low estimate in instructions; evaluate is at 58% of it. The gap is the interval verdicts above: with evaluate:342/354/369 outside the floor the design's own per-read numbers give 0.606 M × 16 + 39.59 M × 8 = 326 M for evaluate, against 247.5 M measured.

The board read in attacked (this.at(source) === color * 2 after the knight delta), from the disassembly of both arms: with the fact off the hot path is 20 instructions up to the load (field load, band, type word, ek_prefix bound, slot math, load), followed by the ?? test; with it on it is 9, and there is no ??:

mov    rdx,[rip+…]            ; field load
mov    rcx,r9
vmovq  xmm0,[rcx+rdx+0x200010]
vmovq  rcx,xmm0
bzhi   rcx,rcx,r12            ; and POINTER_MASK
test   BYTE PTR [rcx-0x7],0x80 ; forwarded?
jne    cold
mov    eax,eax
vmovsd xmm0,[rcx+rax*8+0x18]

Chess.attacked$sig is 986 instructions with the fact on and 1 169 off. Tier blocks per function (on / off), read from the IR: attacked 7 in-floor reads and no ?? (off: 7 ??, 14 guard chains); make 2 forwarding tests, 1 capacity bound, 1 hole test, 1 ?? (at(from) in the floor, at(captureSquare) not; off: 2 ??, 4 guard chains); generatePseudo 15 reads, 3 of them bounded (off: 30 guard chains, 15 ??).

Size (every executable section; on vs off)

.text, perry_js_text, .init, .plt, .plt.got, .fini.

No section of any program grows. Per symbol: skin's symbol table is identical on and off; tssrc differs in one function (addMissingAwait.ts getDeclarationSiteFix, 2 964 B on against 3 083 B off); Supabase differs in one closure (functions/new/new.handler.ts closure 31, 42 815 B on against 42 808 B off: +7 B, not looked into, inside the section's padding since the section sizes are equal).

Departures from the design, and what is not done

• Board reads lose the hole test and the ?? through b1's export-time in_floor, not through ElemUndef. C2's departure stands for direct reads: C1's ElemUndef takes the hole's undefined from hole(t), which every index store marks, so a direct read of a stored-into array (whitePawns[file], and a direct this.board[i]) is Number-or-undefined in the facts and keeps its ?? and number test. Chess reads its board only through at, so that does not cost C3 anything. The solver change (a store of a non-undefined value into a slot below the dense floor creates no hole) is not in this PR.
• The Number claim of an in-floor call is rep.elem, not number_element_reads (C2's rule for direct reads). The body's read node holds the undefined of the other callers' keys, so number_element_reads can never say Number for it. It is the same solver fact (the element nodes hold only Numbers), tested per read by the witness's element test, and P3 B3 is merged. Direct reads keep C2's rule.
• FieldReadCall.in_floor reaches codegen as the floor (FactsFieldReadCall.in_floor: Option<u32>), not as a bool. The floor wpfacts proved the key below is over the Arrays the method's read can read; codegen's FieldProof.array is over the receiver binding's classes. They agree in every program measured, but the witness tests the key against the floor the claim was made for.
• FieldReadCall.array is the rep of the method's read receiver, not FieldFacts::rep of the call's receiver classes: wpfacts has the receiver node there, not codegen's class set. Codegen still requires FieldProof.array (with finding 8's hard test) for the same read.
• An in-floor call over Boxed elements with a ?? L keeps the read it had (bound, hole test, ??). A reader without a default (return this.f[k]) is in the floor for any element kind.
• A call whose index reads a field (this.at(this.ep - 16)) is not a b1 call in codegen (b1's admission wants an inert index: main's rule), so wpfacts' in-floor verdict for it has no consumer.
• Not in the floor because of the key interval (the table above): evaluate:342/354/369, generatePseudo:590 and 741. Follow-ups in the range analysis, each a solver change with its own census: (1) the widening of a sum of two growing operands, (2) a counter write in a branch that always leaves does not end the narrowed reads after the branch. Per the design's per-read numbers (in the floor 16, outside 8) they are worth about 8 instructions on 39.6 M reads of the evaluate workload (about −10%) and on the 80.1 M evaluate reads of search (about −1.9%), plus generatePseudo's at(from). Not measured.
• Fixtures. 11 (field reassignment with another floor, K-FS3 this[name] = other) and the negative controls (stored undefined, a null field, no fused fill, a sparse store past the end, delete of an element, a length store, a deleted field, an overriding subclass, string elements, fraction/NaN/-0 keys) are test_array_reps_fields.ts; 13 is …_fields_gc.ts; 14 is …_fields_growth.ts (push in the reading loop, and one store far past the capacity between reads).
• IR assertions are unit tests on injected facts (proven_array_tests.rs: the in-floor call of a growable and of a fixed board, the call outside the floor, the direct field read, a Boxed field changes nothing, the join). The chess claims above are read from its IR and disassembly by hand.
• Mac: not built. One cargo check --tests ran there on an early commit and stopped at a test-only error in perry-wpfacts before reaching perry-codegen; nothing later was compiled on the Mac.